This invention relates generally to automated design verification, and in particular to more efficient use of binary decision diagrams to perform automated symbolic model checking for very large scale integrated circuit designs and other finite state systems.
Modern design of very large-scale integrated circuits often involves years of research and the efforts of hundreds of engineers. Automated formal verification methods are an essential part of the design effort, reducing errors, lost time and risk to financial investment. Formal verification involves building a finite model of a system as a set of states and state transitions and checking that a desired property holds in the model. An exhaustive search of all possible states of the model may be performed in order to verify a desired property.
As the size and complexity of designs increase, much effort is expended to improve the efficiency of automated formal verification methods. One technique used in symbolic model checking to improve efficiency is to employ binary decision diagrams (BDDs). A BDD is a directed acyclic graph that represents a Boolean expression. For each Boolean variable, there are two outgoing edges representing true or false assignments to the variable. The use of BDDs permits computation times, which are some polynomial function of the number of expression variables. Alternative representations such as clauses or truth tables require execution times, which are some exponential function of the number of expression variables. Therefore, use of BDDs has been popular in the formal verification community since the late 1980""s.
BDDs, however, are not without drawbacks. The ordering of variables is critical to an efficient use of BDDs. Poor variable ordering can increase a BDDs size and cause exponential execution times. One method for symbolic model checking using BDDs comes from Carnegie Mellon University and is known as Symbolic Model Verifier (SMV).
Alternatively SMV uses a well known heuristic based procedure named simplify_assuming that is aimed at reducing BDD representations by simplifying a predicate using an invariant assumption but introduces a proof obligation, which must also be verified. Since the assumption is static it may also be ineffective in pruning a model.
Over the years, techniques have been developed to improve performance and capacity of BDD-based algorithms. One technique is called Cone of Influence (COI) reduction. In COI reduction, an abstraction is built for a circuit model consisting of next state functions only for variables in the dependency closure of variables of interest in the circuit specification. One drawback is that all variables in the dependency closure do not necessarily influence the variables of interest in the circuit specification. A second drawback is that the abstraction that is built and used for each model-checking step may include portions that are useful in only a few of the model checking steps. Therefore needless extra computations are potentially performed, resulting in little benefit to the circuit verification.
Some methods have attempted to improve upon COI reduction by starting from a small portion of the dependency closure and extending the portion only when model checking fails to produce a satisfactory result. But these techniques also perform unnecessary computations on portions that are not relevant to the particular model-checking step being performed.
One method called the bounded cone of influence (BCOI) was proposed by A. Biere et al for symbolic model checking without BDDs [A. Biere, E. Clark, R. Raimi, and Y. Zhu; Verifying safety properties of a PowerPC(trademark) microprocessor using symbolic model checking without BDDs; CAV""99; 1999]. However, even the BCOI method potentially includes irrelevant variables in the abstraction it builds, and the technique is not applicable to improve the widely used BDD-based approaches.